A:es_realizer{i:l}. R-self-interface(A)  R-interface-compat(A; A) 

latex

Definitions

band(p; q), Rsends-T(x1), Rsends-dt(x1), Rsends-l(x1), Rsends-knd(x1), let x = a in b(x), x. t(x), Reffect?(x1), Rsends?(x1), b, prop{i:l}, ff, b, tt, t  T, True, if b then t else f fi , R-interface-compat(A; B), P  Q, x:A. B(x), R-self-interface(R), x(s), False, es_realizer{i:l}, P  Q, P  Q, Unit, , Rrframe(loc; x; L), Rbframe(loc; k; L), Raframe(loc; k; L), Rpre(loc; ds; a; p; P), Rsends(ds; knd; T; l; dt; g), Reffect(loc; ds; knd; T; x; f), Rsframe(lnk; tag; L), Rframe(loc; T; x; L), Rinit(loc; T; x; v), Rplus(left; right), Rnone,

Lemmas

not functionality wrt iff, assert-eq-lnk, lnk wf, eq lnk wf, isrcv wf, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, Reffect wf, Rsframe wf, Rframe wf, Rinit wf, Rplus wf, Rnone wf, true wf, false wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf, es realizer wf, R-self-interface wf, btrue wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, Reffect? wf, eqtt to assert, bool wf, Rsends? wf